\begin{tabbing}
es{-}secret{-}server\=\{\$table:ut2, \$encrypt:ut2, \$decrypt:ut2\}\+
\\[0ex](${\it es}$; $T$; $L$; $i$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$let \=${\it ds}$\= = "\$table" : secret{-}table($T$) in\+\+
\\[0ex]($\uparrow$es{-}isconst(${\it es}$;$i$;"\$table"))
\-\\[0ex]\& l\_all($L$;IdLnk;$l$.destination($l$) = $i$ $\in$ Id
\\[0ex]\& es{-}kind{-}sends{-}iff(${\it es}$;rcv($l$,"\$encrypt");:($\mathbb{N}$ + Atom1)
\\[0ex]$\times$ data($T$);lnk{-}inv($l$);"\$encrypt";:$\mathbb{N}$ $\times$ Atom1;${\it ds}$;$e$.next(es{-}when(${\it es}$; "\$table"; $e$)))
\\[0ex]\& \=es{-}kind{-}sends{-}iff(${\it es}$;rcv($l$,"\$decrypt");:($\mathbb{N}$ + Atom1)\+
\\[0ex]$\times$ Atom1;lnk{-}inv($l$);"\$decrypt";data($T$);${\it ds}$;$e$.decrypt(es{-}when
\\[0ex](${\it es}$; "\$table"; $e$);es{-}val(${\it es}$; $e$))))
\-\\[0ex]\& (\=es{-}frame(${\it es}$;$i$;map($\lambda$$l$.rcv($l$,"\$encrypt");$L$);"\$table";secret{-}table($T$))\+
\\[0ex]c$\wedge$ \=(l\_all($L$;IdLnk;$l$.effect{-}p(${\it es}$;$i$;${\it ds}$;rcv($l$,"\$encrypt");:($\mathbb{N}$ + Atom1)\+
\\[0ex]$\times$ data($T$);"\$table";$\lambda$$s$,$v$. encrypt($s$."\$table";$v$)))
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.$\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex](es{-}leaks(${\it es}$;$e$;"\$table";${\it e'}$)
\\[0ex]$\Rightarrow$ \=l\_exists($L$;IdLnk;$l$.(\=es{-}kind(${\it es}$; $e$)\+\+
\\[0ex]=
\\[0ex]rcv($l$,"\$encrypt")
\\[0ex]$\in$ Knd
\-\\[0ex]\& es{-}kind(${\it es}$; ${\it e'}$) = rcv(lnk{-}inv($l$),"\$encrypt") $\in$ Knd)
\\[0ex]$\vee$ \=(es{-}kind(${\it es}$; $e$) = rcv($l$,"\$decrypt") $\in$ Knd\+
\\[0ex]\& \=es{-}kind(${\it es}$; ${\it e'}$)\+
\\[0ex]=
\\[0ex]rcv(lnk{-}inv($l$),"\$decrypt")
\\[0ex]$\in$ Knd))))
\-\-\-\-\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.$\neg$es{-}copies(${\it es}$;$e$;"\$table"))
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.($\uparrow$es{-}first(${\it es}$; $e$))\+
\\[0ex]$\Rightarrow$ \=(atoms{-}distinct(es{-}when(${\it es}$; "\$table"; $e$))\+
\\[0ex]\& ptr(es{-}when(${\it es}$; "\$table"; $e$)) = 0 $\in$ $\mathbb{N}$
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$, $j$:Id.\+
\\[0ex]($n$ $<$ $\parallel$es{-}when(${\it es}$; "\$table"; $e$)$\parallel$ )
\\[0ex]$\Rightarrow$ es{-}atom(${\it es}$;$j$;st{-}atom(es{-}when(${\it es}$; "\$table"; $e$);$n$))
\\[0ex]$\Rightarrow$ ($j$ = $i$ $\in$ Id))))))
\-\-\-\-\-\-
\end{tabbing}